CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[1]∨LENGTH[5];

ELAPSED-TIME =124351

NIL 1 5
1 S(THM2,THM3,THM3,THM1);3 4
3 S(THM3,THM1,THM2,THM3);5 6
4 S(z,u,x,y)⊃S(x,y,z,u);A2
5 S(y,x,z,u)⊃S(x,y,z,u);A3
6 S(THM1,THM3,THM2,THM3);THM